R:Realizer. R-Feasible(R)  R-base-ma(R)  MsgA 

latex

Definitions

x:A. B(x), P  Q, t  T, R-base-ma(R), State(ds), DeclaredType(ds;x), Prop, x. t(x), Valtype(da;k), S  T, S  T, Top, if b t else f fi, true, SQType(T), {T}, false, P  Q, T, True, P & Q, P  Q, Realizer, Unit, x(s), , R-Feasible(R), rcv(l,tg), b, isrcv(k), lnk(k), tag(k), isl(x), 1of(t), outl(x), 2of(t), , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , State(ds), sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x

Lemmas

unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, ma-empty wf, R-Feasible wf, Rnone wf, Rplus wf, ma-single-init wf, Rinit wf, ma-single-frame wf, Rframe wf, ma-single-sframe wf, Rsframe wf, ma-single-effect wf, fpf-single wf, fpf-cap-single1, Kind-deq wf, fpf-cap wf, id-deq wf, ma-valtype wf, ma-state wf, Reffect wf, ma-single-sends wf, fpf-join wf, lnk-decl wf, rcv wf, fpf-cap-single-join, Rsends wf, ma-single-pre wf, Rpre wf, ma-single-aframe wf, Raframe wf, ma-single-bframe wf, Rbframe wf, ma-single-rframe wf, Rrframe wf, es realizer wf, fpf-join-cap-sq, top wf, fpf-trivial-subtype-top, fpf-dom wf, bool wf, eqtt to assert, fpf-single-dom, Knd sq, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, lnk-decl-cap, subtype rel self, squash wf, true wf